Nuprl Lemma : Konig_wf
11,40
postcript
pdf
k
:
. Konig(
k
)
latex
Definitions
,
t
T
,
Type
,
{
x
:
A
|
B
(
x
)}
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
#$n
,
{
i
..
j
}
,
A
B
,
S
T
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
i
j
<
k
,
suptype(
S
;
T
)
,
<
a
,
b
>
,
f
(
a
)
,
b
,
x
:
A
B
(
x
)
,
A
,
P
Q
,
a
<
b
,
False
,
,
,
Konig(
k
)
Lemmas
bool
wf
,
not
wf
,
assert
wf
,
le
wf
,
int
seg
wf
,
nat
wf
origin
k:
. Konig(k) 
k:. Konig(k) T
B(x)x:A. B(x)
}
B
T
x:A. B(x) j < k
b
B(x)
A
Q